package tr.edu.ege.kipler.satisfiability.clash;

import java.util.HashSet;
import java.util.Set;

import tr.edu.ege.kipler.satisfiability.container.ABox;
import tr.edu.ege.kipler.satisfiability.container.DependencyManager;
import tr.edu.ege.kipler.satisfiability.container.Individual;
import tr.edu.ege.kipler.satisfiability.container.WorldConstraintSystem;
import tr.edu.ege.kipler.satisfiability.container.operational.DisjointIndividualDetector;
import tr.edu.ege.kipler.syntax.atomicformula.ConceptAssertion;
import tr.edu.ege.kipler.syntax.atomicformula.Formula;
import tr.edu.ege.kipler.syntax.atomicformula.SameIndividualAssertion;
import tr.edu.ege.kipler.syntax.concept.QualifiedNoRestriction;

/**
 * 
 * @author İnanç Seylan
 *
 */
public class InstantQNRClashDetectionStrategy implements ClashDetectionStrategy {

	private Set<WorldConstraintSystem> dependencySet = new HashSet<WorldConstraintSystem>();

	private ABox abox;

	private Set<Individual> problematicDisjointIndividuals;

	private Set<Individual> neighbors;

	public InstantQNRClashDetectionStrategy(Set<Individual> neighbors) {
		this.neighbors = neighbors;
	}

	public String getExplanation() {
		return "QR";
	}

	public Set<WorldConstraintSystem> getDependencySet() {
		return dependencySet;
	}

	public boolean hasClash(ABox abox, Formula formula) {
		boolean result = false;
		this.abox = abox;
		if (formula instanceof ConceptAssertion) {
			ConceptAssertion ca = (ConceptAssertion) formula;
			result = checkConceptAssertion(ca);
		}
		return result;
	}

	protected ABox getABox() {
		return abox;
	}

	protected void setABox(ABox abox) {
		this.abox = abox;
	}

	/**
	 * @param abox
	 * @param result
	 * @param ca
	 * @return
	 */
	private boolean checkConceptAssertion(ConceptAssertion ca) {
		Individual indv = abox.getIndividual(ca.getName());
		boolean result = false;
		if (ca.getConcept() instanceof QualifiedNoRestriction) {
			QualifiedNoRestriction qr = (QualifiedNoRestriction) ca
					.getConcept();
			if (atMostViolated(qr, indv)) {
				result = true;
			}
		}
		return result;
	}

	protected boolean atMostViolated(QualifiedNoRestriction qr, Individual indv) {
		boolean result = false;
		if (neighbors.size() > qr.getNo()
				&& isClashConditionDetected(qr, neighbors)) {
			result = true;
			manageDependency(qr, indv);
		}
		return result;
	}

	/**
	 * @param qr
	 * @param neighbors
	 */
	private boolean isClashConditionDetected(QualifiedNoRestriction qr,
			Set<Individual> neighbors) {
		boolean result = false;
		DisjointIndividualDetector detector = new DisjointIndividualDetector(
				abox, neighbors);
		if (detector.hasSetWithMinCardinality(qr.getNo() + 1)) {
			result = true;
			problematicDisjointIndividuals = detector.getResult();
		}
		return result;
	}

	/**
	 * @param qr
	 * @param owner
	 */
	private void manageDependency(QualifiedNoRestriction qr, Individual owner) {
		getDependencySet().clear();
		DependencyManager depMan = abox.getWorld().getWcs().getData()
				.getDependencyManager();
		for (Individual indv : problematicDisjointIndividuals) {
			getDependencySet().addAll(
					depMan.getDependencies(new ConceptAssertion(
							qr.getConcept(), indv.getName())));
			for (Individual otherIndv : problematicDisjointIndividuals) {
				if (!indv.equals(otherIndv)) {
					getDependencySet().addAll(
							depMan.getDependencies(new SameIndividualAssertion(
									indv.getName(), otherIndv.getName())
									.toggleNegated()));
				}
			}
		}
		/*
		 * There is no need to consider the dependency information of edges from
		 * the owner to the neighbors because the dependency information for
		 * those edges are already included in the labels of neighbors.
		 */
		getDependencySet().addAll(
				depMan
						.getDependencies(new ConceptAssertion(qr, owner
								.getName())));
	}

}
